package trabajoISW2.domain.contracts;

import java.util.List;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Book;
import trabajoISW2.domain.models.ICatalogModel;

public interface ICatalog extends ICatalogModel{
	

	
	@Pre("books !=null #IllegalArgumentException")
	@Pos("getBooks().compare(books) == 0")
	public void setBooks(List<Book> books);
	
	@Query
	public List<Book>  getBooks();
	
	@Query
	@Pre("authorId >= 0 && authorId <= Integer.MAX_VALUE #WrongIdException")
	@Pos({"areBooksAuthor(searchByAuthorId(authorID),authorId)"})
	public List<Book> searchByAuthorId (int authorId);
	
	
	@Query
	@Pre("title.compareTo(\"\") != 0 && title !=null #WrongNameException")
	@Pos({"areBooksTitle(searchByTitle(title), title)"})
	public List<Book> searchByTitle (String title);
	
	@Query
	@Pre({"isbn.length() == 10 || isbn.length() == 13 #IllegalArgumentException", "isbn != null #IllegalArgumentException"})
	@Pos("getBook(isbn).getIsbn() == isbn")
	public Book getBook (String isbn);
	
	@Pre("b.compare(null) != 0 #IllegalArgumentException")
	@Pos({"!getBooks().contains(book)@pre ==> getBooks().contains(book) && getBooks().size() == getBooks().size()@pre + 1",
		  "getBooks().contains(book)@pre ==> getBooks().size() == getBooks().size()@pre"})
	public boolean addBook(Book b);
	
	@Pre("b.compare(null) != 0 #IllegalArgumentException")
	@Pos({"getBooks().contains(book)@pre ==> !getBooks().contains(book) && getBooks().size() == getBooks().size()@pre -1",
		  "!getBooks().contains(book)@pre ==> getBooks().size()@pre == getBooks.size()"})
    public boolean removeBook(Book b);
	

}
